d-comp(D; v; sched; dec; d)(t,f)
== let s = i.if (t = 0) then x.M(i).init(x)?v(i,x) else (f((t - 1),i)).1 fi  in
== let si.let si = s(i) in
== let si.let silet w = d-partial-world(D;f;t;s;d) in
== let si.let silet wlet a = case sched(i)
== let si.let silet wlet of inl(f) => case f(t)
== let si.let silet wlet of inl(f) => of inl(l) => if destination(l) = i  0 <z ||queue(l;t)||
== let si.let silet wlet of inl(f) => of inl(l) => then doact(rcv(l,mtag(hd(queue(l;t))))
== let si.let silet wlet of inl(f) => of inl(l) => then doact;mval(hd(queue(l;t))))
== let si.let silet wlet of inl(f) => of inl(l) => else null
== let si.let silet wlet of inl(f) => of inl(l) => fi 
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(dec
== let si.let silet wlet of inl(f) => o| inr(a) => if isl((i
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(,a
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(,w-knum(w;i;locl(a);t)
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(,read-state(si)))
== let si.let silet wlet of inl(f) => o| inr(a) => then doact(inr a 
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(dec
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl((i
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(,a
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(,w-knum(w;i;locl(a);t)
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(,read-state(si))))
== let si.let silet wlet of inl(f) => o| inr(a) => else null
== let si.let silet wlet of inl(f) => o| inr(a) => fi 
== let si.let silet wlet o| inr(x) => null in
== let si.let silet wlet olet m = if isl(a)
== let si.let silet wlet olet then []
== let si.let silet wlet olet else filter(m.source(mlnk(m)) = i
== let si.let silet wlet olet else filter;M(i).sends(outr(a).1,read-state(si),outr(a).2))
== let si.let silet wlet olet fi  in
== let si.let silet wlet olet flet s' = if isl(a)
== let si.let silet wlet olet flet then si
== let si.let silet wlet olet flet else x.M(i).ef(outr(a).1,x,read-state(si),outr(a).2)?si(x)
== let si.let silet wlet olet flet fi  in <shift-state(s'), a, m> 

latex

---

clarification:

d-comp(D; v; sched; dec; d)(t,f)
== let s = i.if (t = 0) then x.d-m(D; i).init(x)?v(i,x) else (f((t - 1),i)).1 fi  in
== let si.let si = s(i) in
== let si.let silet w = d-partial-world(D;f;t;s;d) in
== let si.let silet wlet a = case sched(i)
== let si.let silet wlet of inl(f) => case f(t)
== let si.let silet wlet of inl(f) => of inl(l) => if destination(l) = i
== let si.let silet wlet of inl(f) => of inl(l) => if  0 <z ||w-queue(w; l; t)||
== let si.let silet wlet of inl(f) => of inl(l) => then doact(rcv(l,mtag(hd(w-queue(w; l; t))))
== let si.let silet wlet of inl(f) => of inl(l) => then doact;mval(hd(w-queue(w; l; t))))
== let si.let silet wlet of inl(f) => of inl(l) => else null
== let si.let silet wlet of inl(f) => of inl(l) => fi 
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(dec
== let si.let silet wlet of inl(f) => o| inr(a) => if isl((i
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(,a
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(,w-knum(w;i;locl(a);t)
== let si.let silet wlet of inl(f) => o| inr(a) => if isl(,read-state(si)))
== let si.let silet wlet of inl(f) => o| inr(a) => then doact(inr a 
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(dec
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl((i
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(,a
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(,w-knum(w;i;locl(a);t)
== let si.let silet wlet of inl(f) => o| inr(a) => then doact;outl(,read-state(si))))
== let si.let silet wlet of inl(f) => o| inr(a) => else null
== let si.let silet wlet of inl(f) => o| inr(a) => fi 
== let si.let silet wlet o| inr(x) => null in
== let si.let silet wlet olet m = if isl(a)
== let si.let silet wlet olet then []
== let si.let silet wlet olet else filter(m.source(mlnk(m)) = i
== let si.let silet wlet olet else filter;d-m(D; i).sends(outr(a).1,read-state(si),outr(a).2))
== let si.let silet wlet olet fi  in
== let si.let silet wlet olet flet s' = if isl(a)
== let si.let silet wlet olet flet then si
== let si.let silet wlet olet flet else x.d-m(D; i).ef(outr(a).1,x,read-state(si),outr(a).2)?si(x)
== let si.let silet wlet olet flet fi  in <shift-state(s'), a, m> 

latex

Definitions

(i = j), M.init(x)?v, n - m, d-partial-world(D;f;t';s;d), case b of inl(x) => s(x) | inr(y) => t(y), p  q, i = j, destination(l), i <z j, #$n, ||as||, rcv(l,tg), mtag(m), mval(m), hd(l), queue(l;t), doact(k;v), inr x , outl(x), w-knum(w;i;k;t), locl(a), null, [], filter(P;l), a = b, source(l), mlnk(m), M.sends(k,s,v), let x = a in b(x), if b then t else f fi , isl(x), x.A(x), M.ef(k,x,s,v)?w, M(i), t.1, read-state(s), t.2, outr(x), f(a), shift-state(s), <a, b>